/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.mit.csail.sdg.alloy4compiler.ast;

import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorSyntax;
import edu.mit.csail.sdg.alloy4.ErrorType;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4.JoinableList;
import edu.mit.csail.sdg.alloy4.Util;
import edu.mit.csail.sdg.alloy4compiler.ast.Type.ProductType;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig;
import static edu.mit.csail.sdg.alloy4compiler.ast.Sig.SIGINT;
import static edu.mit.csail.sdg.alloy4compiler.ast.Type.EMPTY;

/**
 * Immutable; represents an expression of the form (x OP y).
 *
 * <p> <b>Invariant:</b>  type!=EMPTY => (this.mult!=1)
 * <p> <b>Invariant:</b>  type!=EMPTY => (this.mult==2 => this.op is one of the 17 arrow operators)
 * <p> <b>Invariant:</b>  type!=EMPTY => (left.mult!=1)
 * <p> <b>Invariant:</b>  type!=EMPTY => (left.mult==2 => this.op is one of the 17 arrow operators)
 * <p> <b>Invariant:</b>  type!=EMPTY => (right.mult==1 => this.op==IN)
 * <p> <b>Invariant:</b>  type!=EMPTY => (right.mult==2 => (this.op==IN || this.op is one of the 17 arrow operators))
 */

public final class ExprBinary extends Expr {

    /** The binary operator. */
    public final Op op;

    /** The left-hand-side expression. */
    public final Expr left;

    /** The right-hand-side expression. */
    public final Expr right;

    /** Caches the span() result. */
    private Pos span = null;

    //============================================================================================================//

    /** Constructs a new ExprBinary node. */
    private ExprBinary(Pos pos, Pos closingBracket, Op op, Expr left, Expr right, Type type, JoinableList<Err> errors) {
        super(pos,
            closingBracket,
            left.ambiguous || right.ambiguous,
            type,
            (op.isArrow && (left.mult==2 || right.mult==2 || op!=Op.ARROW))?2:0,
            left.weight + right.weight,
            errors);
        this.op=op;
        this.left=left;
        this.right=right;
    }

    //============================================================================================================//

    /** Returns true if we can determine the two expressions are equivalent; may sometimes return false. */
    @Override public boolean isSame(Expr obj) {
        while(obj instanceof ExprUnary && ((ExprUnary)obj).op==ExprUnary.Op.NOOP) obj=((ExprUnary)obj).sub;
        if (obj==this) return true;
        if (!(obj instanceof ExprBinary)) return false;
        ExprBinary x=(ExprBinary)obj;
        return op==x.op && left.isSame(x.left) && right.isSame(x.right);
    }

    //============================================================================================================//

    /**
     * Convenience method that generates a type error with "msg" as the message,
     * and includes the left and right bounding types in the message.
     */
    private static ErrorType error(Pos pos, String msg, Expr left, Expr right) {
        return new ErrorType(pos, msg+"\nLeft type = "+left.type+"\nRight type = "+right.type);
    }

    //============================================================================================================//

    /**
     * Convenience method that generates a type warning with "msg" as the message,
     * and includes the left and right bounding types in the message.
     */
    private ErrorWarning warn(String msg) {
        return new ErrorWarning(pos, msg
        +"\nLeft type = " + Type.removesBoolAndInt(left.type)
        +"\nRight type = " + Type.removesBoolAndInt(right.type));
    }

    //============================================================================================================//

    /**
     * Convenience method that generates a type warning with "msg" as the message,
     * and includes the parent's relevance type, as well as the left and right bounding types in the message.
     */
    private ErrorWarning warn(String msg, Type parent) {
        return new ErrorWarning(pos, msg
        +"\nParent's relevant type = " + Type.removesBoolAndInt(parent)
        +"\nLeft type = " + Type.removesBoolAndInt(left.type)
        +"\nRight type = " + Type.removesBoolAndInt(right.type));
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public Pos span() {
        Pos p=span;
        if (p==null) span = (p = pos.merge(closingBracket).merge(right.span()).merge(left.span()));
        return p;
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public void toString(StringBuilder out, int indent) {
        if (indent<0) {
            if (op==Op.ISSEQ_ARROW_LONE) out.append("seq "); else { left.toString(out,-1); out.append(' ').append(op).append(' '); }
            right.toString(out,-1);
        } else {
            for(int i=0; i<indent; i++) { out.append(' '); }
            out.append(op).append(" with type=").append(type).append('\n');
            left.toString(out, indent+2);
            right.toString(out, indent+2);
        }
    }

    //============================================================================================================//

    /** This class contains all possible binary operators. */
    public static enum Op {
        /** -&gt;           */  ARROW("->",true),
        /** -&gt;some       */  ANY_ARROW_SOME("->some",true),
        /** -&gt;one        */  ANY_ARROW_ONE("->one",true),
        /** -&gt;lone       */  ANY_ARROW_LONE("->lone",true),
        /** some-&gt;       */  SOME_ARROW_ANY("some->",true),
        /** some-&gt;some   */  SOME_ARROW_SOME("some->some",true),
        /** some-&gt;one    */  SOME_ARROW_ONE("some->one",true),
        /** some-&gt;lone   */  SOME_ARROW_LONE("some->lone",true),
        /** one-&gt;        */  ONE_ARROW_ANY("one->",true),
        /** one-&gt;some    */  ONE_ARROW_SOME("one->some",true),
        /** one-&gt;one     */  ONE_ARROW_ONE("one->one",true),
        /** one-&gt;lone    */  ONE_ARROW_LONE("one->lone",true),
        /** lone-&gt;       */  LONE_ARROW_ANY("lone->",true),
        /** lone-&gt;some   */  LONE_ARROW_SOME("lone->some",true),
        /** lone-&gt;one    */  LONE_ARROW_ONE("lone->one",true),
        /** lone-&gt;lone   */  LONE_ARROW_LONE("lone->lone",true),
        /** isSeq-&gt;lone  */  ISSEQ_ARROW_LONE("isSeq->lone",true),
        /** .               */  JOIN(".",false),
        /** &lt;:           */  DOMAIN("<:",false),
        /** :&gt;           */  RANGE(":>",false),
        /** &amp;           */  INTERSECT("&",false),
        /** ++              */  PLUSPLUS("++",false),
        /** +               */  PLUS("+",false),
        /** -               */  MINUS("-",false),
        /** multiply        */  MUL("*",false),
        /** divide          */  DIV("/",false),
        /** remainder       */  REM("%",false),
        /** =               */  EQUALS("=",false),
        /** &lt;            */  LT("<",false),
        /** =&lt;           */  LTE("<=",false),
        /** &gt;            */  GT(">",false),
        /** &gt;=           */  GTE(">=",false),
        /** &lt;&lt;        */  SHL("<<",false),
        /** &gt;&gt;        */  SHA(">>",false),
        /** &gt;&gt;&gt;    */  SHR(">>>",false),
        /** in              */  IN("in",false),
        /** &amp;&amp;      */  AND("&&",false),
        /** ||              */  OR("||",false),
        /** &lt;=&gt;       */  IFF("<=>",false);

        /**
         * The constructor.
         * @param label - the label (for printing debugging messages)
         * @param isArrow - true if this operator is one of the 17 arrow operators
         */
        private Op(String label, boolean isArrow) {
            this.label=label;
            this.isArrow=isArrow;
        }

        /** The human readable label for this operator. */
        private final String label;

        /**
         * True if and only if this operator is the Cartesian product "->", a "seq" multiplicity,
         * or is a multiplicity arrow of the form "?->?".
         */
        public final boolean isArrow;

        /**
         * Constructs a new ExprBinary node.
         * @param pos - the original position in the source file (can be null if unknown)
         * @param left - the left hand side expression
         * @param right - the right hand side expression
         */
        public final Expr make(Pos pos, Pos closingBracket, Expr left, Expr right) {
            switch(this) {
              case AND: return ExprList.makeAND(left, right);
              case OR: return ExprList.makeOR(left, right);
              case DOMAIN: {
                // Special optimization
                Expr f = right.deNOP();
                if (f instanceof Field && ((Field)f).sig==left.deNOP()) return right;
                break;
              }
              case MUL: case DIV: case REM: case LT: case LTE: case GT: case GTE: case SHL: case SHR: case SHA: {
                left = left.typecheck_as_int();
                right = right.typecheck_as_int();
                break;
              }
              case IFF: {
                left = left.typecheck_as_formula();
                right = right.typecheck_as_formula();
                break;
              }
              case PLUS: case MINUS: case EQUALS: {
                Type a=left.type, b=right.type;
                if (a.hasCommonArity(b) || (a.is_int && b.is_int)) break;
                if (Type.SIGINT2INT) {
                    if (a.is_int && b.intersects(SIGINT.type)) { right=right.cast2int(); break; }
                    if (b.is_int && a.intersects(SIGINT.type)) { left=left.cast2int(); break; }
                }
                if (Type.INT2SIGINT) {
                    if (a.is_int && b.hasArity(1)) { left=left.cast2sigint(); break; }
                    if (b.is_int && a.hasArity(1)) { right=right.cast2sigint(); break; }
                }
                break;
              }
              default: {
                left = left.typecheck_as_set();
                right = right.typecheck_as_set();
              }
            }
            Err e=null;
            Type type=EMPTY;
            JoinableList<Err> errs = left.errors.join(right.errors);
            if (errs.isEmpty()) switch(this) {
              case LT: case LTE: case GT: case GTE: case AND: case OR: case IFF:
                  type = Type.FORMULA;
                  break;
              case MUL: case DIV: case REM: case SHL: case SHR: case SHA:
                  type = Type.INT;
                  break;
              case PLUSPLUS:
                  type = left.type.unionWithCommonArity(right.type);
                  if (type==EMPTY) e=error(pos, "++ can be used only between two expressions of the same arity.", left, right);
                  break;
              case PLUS: case MINUS: case EQUALS:
                  if (this==EQUALS) {
                     if (left.type.hasCommonArity(right.type) || (left.type.is_int && right.type.is_int)) {type=Type.FORMULA; break;}
                  } else {
                     type = (this==PLUS ? left.type.unionWithCommonArity(right.type) : left.type.pickCommonArity(right.type));
                     if (left.type.is_int && right.type.is_int) type=Type.makeInt(type);
                     if (type!=EMPTY) break;
                  }
                  e=error(pos, this+" can be used only between 2 expressions of the same arity, or between 2 integer expressions.", left, right);
                  break;
              case IN:
                  type=(left.type.hasCommonArity(right.type)) ? Type.FORMULA : EMPTY;
                  if (type==EMPTY) e=error(pos,this+" can be used only between 2 expressions of the same arity.", left, right);
                  break;
              case JOIN:
                  type=left.type.join(right.type);
                  if (type==EMPTY) return ExprBadJoin.make(pos, closingBracket, left, right);
                  break;
              case DOMAIN:
                  type=right.type.domainRestrict(left.type);
                  if (type==EMPTY) e=new ErrorType(left.span(),
                     "This must be a unary set, but instead it has the following possible type(s):\n"+left.type);
                  break;
              case RANGE:
                  type=left.type.rangeRestrict(right.type);
                  if (type==EMPTY) e=new ErrorType(right.span(),
                     "This must be a unary set, but instead it has the following possible type(s):\n"+right.type);
                  break;
              case INTERSECT:
                  type=left.type.intersect(right.type);
                  if (type==EMPTY) e=error(pos,"& can be used only between 2 expressions of the same arity.", left, right);
                  break;
              default:
                  type=left.type.product(right.type);
            }
            if ((isArrow && left.mult==1) || (!isArrow && left.mult!=0))
                errs = errs.append(new ErrorSyntax(left.span(), "Multiplicity expression not allowed here."));
            if ((isArrow && right.mult==1) || (!isArrow && this!=Op.IN && right.mult!=0))
                errs = errs.append(new ErrorSyntax(right.span(), "Multiplicity expression not allowed here."));
            if (errs.isEmpty() && e==null && left.type.is_bool && right.type.is_bool && (this==AND || this==OR)) {
                if (this==AND) return ExprList.makeAND(left, right); else return ExprList.makeOR(left, right);
            }
            return new ExprBinary(pos, closingBracket, this, left, right, type, errs.append(e));
        }

        /** Returns the human readable label for this operator. */
        @Override public final String toString() { return label; }

        /** Returns the human readable label already encoded for HTML */
        public final String toHTML() { return label.replace("&", "&amp;").replace("<","&lt;").replace(">","&gt;"); }
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public Expr resolve(Type p, Collection<ErrorWarning> warns) {
        if (errors.size()>0) return this;
        ErrorWarning w=null;
        Type a=left.type, b=right.type;
        switch(op) {
          case MUL: case DIV: case REM: case LT: case LTE: case GT: case GTE: case SHL: case SHR: case SHA: {
            a=(b=Type.INT);
            break;
          }
          case AND: case OR: case IFF: {
            a=(b=Type.FORMULA);
            break;
          }
          case EQUALS: {
            p=a.intersect(b);
            if (p.hasTuple()) {a=p; b=p;} else {a=a.pickCommonArity(b); b=b.pickCommonArity(a);}
            if (left.type.is_int && right.type.is_int) {
               a=Type.makeInt(a); b=Type.makeInt(b);
            } else if (warns==null) {
               break;
            } else if (left.type.hasTuple() && right.type.hasTuple() && !(left.type.intersects(right.type))) {
               w=warn("== is redundant, because the left and right expressions are always disjoint.");
            } else if (left.isSame(right)) {
               w=warn("== is redundant, because the left and right expressions always have the same value.");
            }
            break;
          }
          case IN: {
            a=a.pickCommonArity(b);
            b=b.intersect(a);
            if (warns==null) break;
            if (left.type.hasNoTuple() && right.type.hasNoTuple())
               w=warn("Subset operator is redundant, because both subexpressions are always empty.");
            else if (left.type.hasNoTuple())
               w=warn("Subset operator is redundant, because the left subexpression is always empty.");
            else if (right.type.hasNoTuple())
               w=warn("Subset operator is redundant, because the right subexpression is always empty.");
            else if (b.hasNoTuple())
               w=warn("Subset operator is redundant, because the left and right subexpressions are always disjoint.");
            else if (left.isSame(right))
               w=warn("Subset operator is redundant, because the left and right expressions always have the same value.");
            break;
          }
          case INTERSECT: {
            a=a.intersect(p);
            b=b.intersect(p);
            if (warns!=null && type.hasNoTuple()) w=warn("& is irrelevant because the two subexpressions are always disjoint.");
            break;
          }
          case PLUSPLUS: case PLUS: {
            a=a.intersect(p);
            b=b.intersect(p);
            if (op==Op.PLUS && p.is_int) { a=Type.makeInt(a); b=Type.makeInt(b); }
            if (warns==null) break;
            if (a==EMPTY && b==EMPTY)
               w=warn(this+" is irrelevant since both subexpressions are redundant.", p);
            else if (a==EMPTY)
               w=warn(this+" is irrelevant since the left subexpression is redundant.", p);
            else if (b==EMPTY || (op==Op.PLUSPLUS && !right.type.canOverride(left.type)))
               w=warn(this+" is irrelevant since the right subexpression is redundant.", p);
            break;
          }
          case MINUS: {
            a=p;
            b=p.intersect(b);
            if (p.is_int) {
                a=Type.makeInt(a); b=Type.makeInt(b);
            } else if (warns!=null && (type.hasNoTuple() || b.hasNoTuple())) {
                w=warn("- is irrelevant since the right expression is redundant.", p);
            }
            break;
          }
          case JOIN: {
            if (warns!=null && type.hasNoTuple()) w=warn("The join operation here always yields an empty set.");
            a=(b=EMPTY);
            for (ProductType aa: left.type) for (ProductType bb: right.type) if (p.hasArity(aa.arity()+bb.arity()-2)) {
              PrimSig j = aa.get(aa.arity()-1).intersect(bb.get(0));
              if (j != Sig.NONE) for (ProductType cc:p.intersect(aa.join(bb))) if (!cc.isEmpty()) {
                 List<PrimSig> v = new ArrayList<PrimSig>(cc.arity() + 1);
                 for(int i=0; i<cc.arity(); i++) v.add(cc.get(i));
                 v.add(aa.arity()-1, j);
                 a = a.merge(Type.make(v, 0, aa.arity()));
                 b = b.merge(Type.make(v, aa.arity()-1, v.size()));
              }
            }
            if (a==EMPTY || b==EMPTY) { // Continue the best we can; we should have issued a relevance warning elsewhere already.
              a=(b=EMPTY);
              for (ProductType aa: left.type) for (ProductType bb: right.type)
                if (p.hasArity(aa.arity()+bb.arity()-2) && aa.get(aa.arity()-1).intersects(bb.get(0)))
                   {a=a.merge(aa); b=b.merge(bb);}
            }
            if (a==EMPTY || b==EMPTY) { // Continue the best we can; we should have issued a relevance warning elsewhere already.
              a=(b=EMPTY);
              for (ProductType aa: left.type) for (ProductType bb: right.type)
                if (p.hasArity(aa.arity()+bb.arity()-2))
                   {a=a.merge(aa); b=b.merge(bb);}
            }
            break;
          }
          case DOMAIN: {
            // leftType' = {r1 | r1 in leftType and there exists r2 in rightType such that r1<:r2 in parentType}
            // rightType' = {r2 | r2 in rightType and there exists r1 in leftType such that r1<:r2 in parentType}
            if (warns!=null && type.hasNoTuple()) w=warn("<: is irrelevant because the result is always empty.");
            Type leftType=EMPTY, rightType=EMPTY;
            for (ProductType aa:a) if (aa.arity()==1) for (ProductType bb:b) if (p.hasArity(bb.arity()))
                for (ProductType cc:p.intersect(bb.columnRestrict(aa.get(0), 0))) if (!cc.isEmpty()) {
                    leftType  = leftType.merge(cc, 0, 1);
                    rightType = rightType.merge(cc);
                }
            if (leftType==EMPTY || rightType==EMPTY) { // We try to proceed the best we can
                leftType = a.extract(1);
                rightType = b.pickCommonArity(p);
            }
            a=leftType; b=rightType; break;
          }
          case RANGE: {
            // leftType' = {r1 | r1 in leftType and there exists r2 in rightType such that r1:>r2 in parentType}
            // rightType' = {r2 | r2 in rightType and there exists r1 in leftType such that r1:>r2 in parentType}
            if (warns!=null && type.hasNoTuple()) w=warn(":> is irrelevant because the result is always empty.");
            Type leftType=EMPTY, rightType=EMPTY;
            for(ProductType bb:b) if (bb.arity()==1) for(ProductType aa:a) if (p.hasArity(aa.arity()))
                for (ProductType cc:p.intersect(aa.columnRestrict(bb.get(0), aa.arity()-1))) if (!cc.isEmpty()) {
                    leftType  = leftType.merge(cc);
                    rightType = rightType.merge(cc, cc.arity()-1, cc.arity());
                }
            if (leftType==EMPTY || rightType==EMPTY) { // We try to proceed the best we can
               leftType = a.pickCommonArity(p);
               rightType = b.extract(1);
            }
            a=leftType; b=rightType; break;
          }
          default: {
            // leftType'  == {r1 | r1 in leftType and there exists r2 in rightType such that r1->r2 in parentType}
            // rightType' == {r2 | r2 in rightType and there exists r1 in leftType such that r1->r2 in parentType}
            if (warns==null) {
                // do nothing
            } else if (a.hasTuple()) {
                if (b.hasNoTuple()) w=warn("The left expression of -> is irrelevant because the right expression is always empty.");
            } else {
                if (b.hasTuple()) w=warn("The right expression of -> is irrelevant because the left expression is always empty.");
            }
            Type leftType=EMPTY, rightType=EMPTY;
            for (ProductType aa:a) if (!aa.isEmpty())
              for (ProductType bb:b) if (!bb.isEmpty() && p.hasArity(aa.arity()+bb.arity()))
                for (ProductType cc:p.intersect(aa.product(bb))) if (!cc.isEmpty()) {
                   leftType  = leftType.merge(cc, 0, aa.arity());
                   rightType = rightType.merge(cc, aa.arity(), cc.arity());
                }
            // We try to proceed the best we can; we should have issued a relevance warning already.
            if (leftType==EMPTY || rightType==EMPTY) { leftType=a; rightType=b; }
            a=leftType;
            b=rightType;
          }
        }
        Expr left = this.left.resolve(a, warns);
        Expr right = this.right.resolve(b, warns);
        if (w!=null) warns.add(w);
        return (left==this.left && right==this.right) ? this : op.make(pos, closingBracket, left, right);
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    public int getDepth() {
        int a=left.getDepth(), b=right.getDepth();
        if (a>=b) return 1+a; else return 1+b;
    }

    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err { return visitor.visit(this); }

    /** {@inheritDoc} */
    @Override public String getDescription() { return op.toHTML() + " <i>Type = " + type + "</i>"; }

    /** {@inheritDoc} */
    @Override public List<? extends Browsable> getSubnodes() { return Util.asList(left, right); }
}
